\begin{tabbing}
send\_onceR\=\{\$done:ut2, \$tg:ut2, \$b:ut2, \$done1:ut2\}\+
\\[0ex]($T$; $A$; $f$; $l$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$$\oplus$(\=onceR\=\{\$b:ut2, \$done1:ut2\}\+\+
\\[0ex](source($l$))
\-\\[0ex].\=sends locl("\$b")(v:Unit) on $l$:\+
\\[0ex]tagged($\langle$"\$tg"$,\,$$\lambda$$s$,$v$. ($f$($s$("\$done"))).nil$\rangle$.nil,State("\$done" : $A$),v):"\$tg" : $T$
\\[0ex].nil)
\-\-
\end{tabbing}